Report for no_context/combo1.c

Generated on 2023-06-28 04:19:08 by CPAchecker 2.2 / svcomp23

Matches in value-assignements (V): {{numOfValueMatches}}

Matches in edge-description: {{numOfDescriptionMatches}}

Rank
Scope
-V-
{{line.bestrank}}
{{line.desc}}
Precondition (initial variable assignment):

{{precondition}}

{{fault.rank}}. {{fault.score}} Details:
Current values:
Name Value
1
// Automatically generated by cegarmc  
2
//  
3
  
4
extern void __VERIFIER_assume(int);  
5
extern int __VERIFIER_nondet_bool();  
6
extern char __VERIFIER_nondet_char();  
7
extern signed char __VERIFIER_nondet_schar();  
8
extern unsigned char __VERIFIER_nondet_uchar();  
9
extern int __VERIFIER_nondet_int();  
10
extern unsigned int __VERIFIER_nondet_uint();  
11
extern short __VERIFIER_nondet_short();  
12
extern unsigned short __VERIFIER_nondet_ushort();  
13
extern long __VERIFIER_nondet_long();  
14
extern unsigned long __VERIFIER_nondet_ulong();  
15
extern long long __VERIFIER_nondet_longlong();  
16
extern unsigned long long __VERIFIER_nondet_ull();  
17
extern float __VERIFIER_nondet_float();  
18
extern double __VERIFIER_nondet_double();  
19
extern long double __VERIFIER_nondet_longdouble();  
20
extern void * __VERIFIER_nondet_pointer();  
21
  
22
int D_print_i;  
23
int D_print_st;  
24
int D_z;  
25
int N_generate_i;  
26
int N_generate_st;  
27
int S1_addsub_i;  
28
int S1_addsub_st;  
29
int S2_presdbl_i;  
30
int S2_presdbl_st;  
31
int S3_zero_i;  
32
int S3_zero_st;  
33
int count;  
34
int main_clk_ev;  
35
int main_clk_neg_edge;  
36
int main_clk_pos_edge;  
37
int main_clk_req_up;  
38
int main_clk_val;  
39
int main_clk_val_t;  
40
int main_dbl_ev;  
41
int main_dbl_req_up;  
42
int main_dbl_val;  
43
int main_dbl_val_t;  
44
int main_diff_ev;  
45
int main_diff_req_up;  
46
int main_diff_val;  
47
int main_diff_val_t;  
48
int main_in1_ev;  
49
int main_in1_req_up;  
50
int main_in1_val;  
51
int main_in1_val_t;  
52
int main_in2_ev;  
53
int main_in2_req_up;  
54
int main_in2_val;  
55
int main_in2_val_t;  
56
int main_pres_ev;  
57
int main_pres_req_up;  
58
int main_pres_val;  
59
int main_pres_val_t;  
60
int main_sum_ev;  
61
int main_sum_req_up;  
62
int main_sum_val;  
63
int main_sum_val_t;  
64
int main_zero_ev;  
65
int main_zero_req_up;  
66
int main_zero_val;  
67
int main_zero_val_t;  
68
int res;  
69
  
70
void error();  
71
void N_generate();  
72
void S1_addsub();  
73
void S2_presdbl();  
74
void S3_zero();  
75
void D_print();  
76
void eval();  
77
void start_simulation();  
78
  
79
  
80
void error() {  
81
  {  
82
  goto ERROR;  
83
  ERROR: ;  
84
  return;  
85
  }  
86
}  
87
  
88
void N_generate() {  
89
  auto int a;  
90
  auto int b;  
91
  {  
92
    main_in1_val_t = __VERIFIER_nondet_int();  
93
  main_in1_req_up = 1;  
94
    main_in2_val_t = __VERIFIER_nondet_int();  
95
  main_in2_req_up = 1;  
96
  return;  
97
  }  
98
}  
99
  
100
void S1_addsub() {  
101
  auto int a;  
102
  auto int b;  
103
  {  
104
  a = main_in1_val;  
105
  b = main_in2_val;  
106
  main_sum_val_t = a + b;  
107
  main_sum_req_up = 1;  
108
  main_diff_val_t = a - b;  
109
  main_diff_req_up = 1;  
110
  return;  
111
  }  
112
}  
113
  
114
void S2_presdbl() {  
115
  auto int a;  
116
  auto int b;  
117
  auto int c;  
118
  auto int d;  
119
  {  
120
  a = main_sum_val;  
121
  b = main_diff_val;  
122
  main_pres_val_t = a;  
123
  main_pres_req_up = 1;  
124
  c = a + b;  
125
  d = a - b;  
126
  main_dbl_val_t = c + d;  
127
  main_dbl_req_up = 1;  
128
  return;  
129
  }  
130
}  
131
  
132
void S3_zero() {  
133
  auto int a;  
134
  auto int b;  
135
  {  
136
  a = main_pres_val;  
137
  b = main_dbl_val;  
138
  main_zero_val_t = b - (a + a);  
139
  main_zero_req_up = 1;  
140
  return;  
141
  }  
142
}  
143
  
144
void D_print() {  
145
  {  
146
  D_z = main_zero_val;  
147
  return;  
148
  }  
149
}  
150
  
151
void eval() {  
152
  auto int tmp;  
153
  auto int tmp___0;  
154
  auto int tmp___1;  
155
  auto int tmp___2;  
156
  auto int tmp___3;  
157
  {  
158
  {  
159
    while (1) {  
160
      {  
161
        while_0_continue: ;  
162
        if (N_generate_st == 0) {  
163
          }  
164
        else {  
165
          if (S1_addsub_st == 0) {  
166
            }  
167
          else {  
168
            if (S2_presdbl_st == 0) {  
169
              }  
170
            else {  
171
              if (S3_zero_st == 0) {  
172
                }  
173
              else {  
174
                if (D_print_st == 0) {  
175
                  }  
176
                else {  
177
                  goto while_0_break;  
178
                  }  
179
                }  
180
              }  
181
            }  
182
          }  
183
        if (N_generate_st == 0) {  
184
          {  
185
                        tmp = __VERIFIER_nondet_int();  
186
            }  
187
          if (tmp) {  
188
            N_generate_st = 1;  
189
                        N_generate();  
190
            }  
191
          else {  
192
            }  
193
          }  
194
        else {  
195
          }  
196
        if (S1_addsub_st == 0) {  
197
          {  
198
                        tmp___0 = __VERIFIER_nondet_int();  
199
            }  
200
          if (tmp___0) {  
201
            S1_addsub_st = 1;  
202
                        S1_addsub();  
203
            }  
204
          else {  
205
            }  
206
          }  
207
        else {  
208
          }  
209
        if (S2_presdbl_st == 0) {  
210
          {  
211
                        tmp___1 = __VERIFIER_nondet_int();  
212
            }  
213
          if (tmp___1) {  
214
            S2_presdbl_st = 1;  
215
                        S2_presdbl();  
216
            }  
217
          else {  
218
            }  
219
          }  
220
        else {  
221
          }  
222
        if (S3_zero_st == 0) {  
223
          {  
224
                        tmp___2 = __VERIFIER_nondet_int();  
225
            }  
226
          if (tmp___2) {  
227
            S3_zero_st = 1;  
228
                        S3_zero();  
229
            }  
230
          else {  
231
            }  
232
          }  
233
        else {  
234
          }  
235
        if (D_print_st == 0) {  
236
          {  
237
                        tmp___3 = __VERIFIER_nondet_int();  
238
            }  
239
          if (tmp___3) {  
240
            D_print_st = 1;  
241
                        D_print();  
242
            }  
243
          else {  
244
            }  
245
          }  
246
        else {  
247
          }  
248
        }  
249
      }  
250
    while_0_break: ;  
251
    }  
252
  return;  
253
  }  
254
}  
255
  
256
void start_simulation() {  
257
  auto int kernel_st;  
258
  {  
259
  kernel_st = 0;  
260
  if (main_in1_req_up == 1) {  
261
    if (main_in1_val != main_in1_val_t) {  
262
      main_in1_val = main_in1_val_t;  
263
      main_in1_ev = 0;  
264
      }  
265
    else {  
266
      }  
267
    main_in1_req_up = 0;  
268
    }  
269
  else {  
270
    }  
271
  if (main_in2_req_up == 1) {  
272
    if (main_in2_val != main_in2_val_t) {  
273
      main_in2_val = main_in2_val_t;  
274
      main_in2_ev = 0;  
275
      }  
276
    else {  
277
      }  
278
    main_in2_req_up = 0;  
279
    }  
280
  else {  
281
    }  
282
  if (main_sum_req_up == 1) {  
283
    if (main_sum_val != main_sum_val_t) {  
284
      main_sum_val = main_sum_val_t;  
285
      main_sum_ev = 0;  
286
      }  
287
    else {  
288
      }  
289
    main_sum_req_up = 0;  
290
    }  
291
  else {  
292
    }  
293
  if (main_diff_req_up == 1) {  
294
    if (main_diff_val != main_diff_val_t) {  
295
      main_diff_val = main_diff_val_t;  
296
      main_diff_ev = 0;  
297
      }  
298
    else {  
299
      }  
300
    main_diff_req_up = 0;  
301
    }  
302
  else {  
303
    }  
304
  if (main_pres_req_up == 1) {  
305
    if (main_pres_val != main_pres_val_t) {  
306
      main_pres_val = main_pres_val_t;  
307
      main_pres_ev = 0;  
308
      }  
309
    else {  
310
      }  
311
    main_pres_req_up = 0;  
312
    }  
313
  else {  
314
    }  
315
  if (main_dbl_req_up == 1) {  
316
    if (main_dbl_val != main_dbl_val_t) {  
317
      main_dbl_val = main_dbl_val_t;  
318
      main_dbl_ev = 0;  
319
      }  
320
    else {  
321
      }  
322
    main_dbl_req_up = 0;  
323
    }  
324
  else {  
325
    }  
326
  if (main_zero_req_up == 1) {  
327
    if (main_zero_val != main_zero_val_t) {  
328
      main_zero_val = main_zero_val_t;  
329
      main_zero_ev = 0;  
330
      }  
331
    else {  
332
      }  
333
    main_zero_req_up = 0;  
334
    }  
335
  else {  
336
    }  
337
  if (main_clk_req_up == 1) {  
338
    if (main_clk_val != main_clk_val_t) {  
339
      main_clk_val = main_clk_val_t;  
340
      main_clk_ev = 0;  
341
      if (main_clk_val == 1) {  
342
        main_clk_pos_edge = 0;  
343
        main_clk_neg_edge = 2;  
344
        }  
345
      else {  
346
        main_clk_neg_edge = 0;  
347
        main_clk_pos_edge = 2;  
348
        }  
349
      }  
350
    else {  
351
      }  
352
    main_clk_req_up = 0;  
353
    }  
354
  else {  
355
    }  
356
  if (N_generate_i == 1) {  
357
    N_generate_st = 0;  
358
    }  
359
  else {  
360
    N_generate_st = 2;  
361
    }  
362
  if (S1_addsub_i == 1) {  
363
    S1_addsub_st = 0;  
364
    }  
365
  else {  
366
    S1_addsub_st = 2;  
367
    }  
368
  if (S2_presdbl_i == 1) {  
369
    S2_presdbl_st = 0;  
370
    }  
371
  else {  
372
    S2_presdbl_st = 2;  
373
    }  
374
  if (S3_zero_i == 1) {  
375
    S3_zero_st = 0;  
376
    }  
377
  else {  
378
    S3_zero_st = 2;  
379
    }  
380
  if (D_print_i == 1) {  
381
    D_print_st = 0;  
382
    }  
383
  else {  
384
    D_print_st = 2;  
385
    }  
386
  if (main_in1_ev == 0) {  
387
    main_in1_ev = 1;  
388
    }  
389
  else {  
390
    }  
391
  if (main_in2_ev == 0) {  
392
    main_in2_ev = 1;  
393
    }  
394
  else {  
395
    }  
396
  if (main_sum_ev == 0) {  
397
    main_sum_ev = 1;  
398
    }  
399
  else {  
400
    }  
401
  if (main_diff_ev == 0) {  
402
    main_diff_ev = 1;  
403
    }  
404
  else {  
405
    }  
406
  if (main_pres_ev == 0) {  
407
    main_pres_ev = 1;  
408
    }  
409
  else {  
410
    }  
411
  if (main_dbl_ev == 0) {  
412
    main_dbl_ev = 1;  
413
    }  
414
  else {  
415
    }  
416
  if (main_zero_ev == 0) {  
417
    main_zero_ev = 1;  
418
    }  
419
  else {  
420
    }  
421
  if (main_clk_ev == 0) {  
422
    main_clk_ev = 1;  
423
    }  
424
  else {  
425
    }  
426
  if (main_clk_pos_edge == 0) {  
427
    main_clk_pos_edge = 1;  
428
    }  
429
  else {  
430
    }  
431
  if (main_clk_neg_edge == 0) {  
432
    main_clk_neg_edge = 1;  
433
    }  
434
  else {  
435
    }  
436
  if (main_clk_pos_edge == 1) {  
437
    N_generate_st = 0;  
438
    }  
439
  else {  
440
    }  
441
  if (main_clk_pos_edge == 1) {  
442
    S1_addsub_st = 0;  
443
    }  
444
  else {  
445
    }  
446
  if (main_clk_pos_edge == 1) {  
447
    S2_presdbl_st = 0;  
448
    }  
449
  else {  
450
    }  
451
  if (main_clk_pos_edge == 1) {  
452
    S3_zero_st = 0;  
453
    }  
454
  else {  
455
    }  
456
  if (main_clk_pos_edge == 1) {  
457
    D_print_st = 0;  
458
    }  
459
  else {  
460
    }  
461
  if (main_in1_ev == 1) {  
462
    main_in1_ev = 2;  
463
    }  
464
  else {  
465
    }  
466
  if (main_in2_ev == 1) {  
467
    main_in2_ev = 2;  
468
    }  
469
  else {  
470
    }  
471
  if (main_sum_ev == 1) {  
472
    main_sum_ev = 2;  
473
    }  
474
  else {  
475
    }  
476
  if (main_diff_ev == 1) {  
477
    main_diff_ev = 2;  
478
    }  
479
  else {  
480
    }  
481
  if (main_pres_ev == 1) {  
482
    main_pres_ev = 2;  
483
    }  
484
  else {  
485
    }  
486
  if (main_dbl_ev == 1) {  
487
    main_dbl_ev = 2;  
488
    }  
489
  else {  
490
    }  
491
  if (main_zero_ev == 1) {  
492
    main_zero_ev = 2;  
493
    }  
494
  else {  
495
    }  
496
  if (main_clk_ev == 1) {  
497
    main_clk_ev = 2;  
498
    }  
499
  else {  
500
    }  
501
  if (main_clk_pos_edge == 1) {  
502
    main_clk_pos_edge = 2;  
503
    }  
504
  else {  
505
    }  
506
  if (main_clk_neg_edge == 1) {  
507
    main_clk_neg_edge = 2;  
508
    }  
509
  else {  
510
    }  
511
  {  
512
    while (1) {  
513
      {  
514
        while_1_continue: ;  
515
        {  
516
          kernel_st = 1;  
517
                    eval();  
518
          }  
519
        kernel_st = 2;  
520
        if (main_in1_req_up == 1) {  
521
          if (main_in1_val != main_in1_val_t) {  
522
            main_in1_val = main_in1_val_t;  
523
            main_in1_ev = 0;  
524
            }  
525
          else {  
526
            }  
527
          main_in1_req_up = 0;  
528
          }  
529
        else {  
530
          }  
531
        if (main_in2_req_up == 1) {  
532
          if (main_in2_val != main_in2_val_t) {  
533
            main_in2_val = main_in2_val_t;  
534
            main_in2_ev = 0;  
535
            }  
536
          else {  
537
            }  
538
          main_in2_req_up = 0;  
539
          }  
540
        else {  
541
          }  
542
        if (main_sum_req_up == 1) {  
543
          if (main_sum_val != main_sum_val_t) {  
544
            main_sum_val = main_sum_val_t;  
545
            main_sum_ev = 0;  
546
            }  
547
          else {  
548
            }  
549
          main_sum_req_up = 0;  
550
          }  
551
        else {  
552
          }  
553
        if (main_diff_req_up == 1) {  
554
          if (main_diff_val != main_diff_val_t) {  
555
            main_diff_val = main_diff_val_t;  
556
            main_diff_ev = 0;  
557
            }  
558
          else {  
559
            }  
560
          main_diff_req_up = 0;  
561
          }  
562
        else {  
563
          }  
564
        if (main_pres_req_up == 1) {  
565
          if (main_pres_val != main_pres_val_t) {  
566
            main_pres_val = main_pres_val_t;  
567
            main_pres_ev = 0;  
568
            }  
569
          else {  
570
            }  
571
          main_pres_req_up = 0;  
572
          }  
573
        else {  
574
          }  
575
        if (main_dbl_req_up == 1) {  
576
          if (main_dbl_val != main_dbl_val_t) {  
577
            main_dbl_val = main_dbl_val_t;  
578
            main_dbl_ev = 0;  
579
            }  
580
          else {  
581
            }  
582
          main_dbl_req_up = 0;  
583
          }  
584
        else {  
585
          }  
586
        if (main_zero_req_up == 1) {  
587
          if (main_zero_val != main_zero_val_t) {  
588
            main_zero_val = main_zero_val_t;  
589
            main_zero_ev = 0;  
590
            }  
591
          else {  
592
            }  
593
          main_zero_req_up = 0;  
594
          }  
595
        else {  
596
          }  
597
        if (main_clk_req_up == 1) {  
598
          if (main_clk_val != main_clk_val_t) {  
599
            main_clk_val = main_clk_val_t;  
600
            main_clk_ev = 0;  
601
            if (main_clk_val == 1) {  
602
              main_clk_pos_edge = 0;  
603
              main_clk_neg_edge = 2;  
604
              }  
605
            else {  
606
              main_clk_neg_edge = 0;  
607
              main_clk_pos_edge = 2;  
608
              }  
609
            }  
610
          else {  
611
            }  
612
          main_clk_req_up = 0;  
613
          }  
614
        else {  
615
          }  
616
        kernel_st = 3;  
617
        if (main_in1_ev == 0) {  
618
          main_in1_ev = 1;  
619
          }  
620
        else {  
621
          }  
622
        if (main_in2_ev == 0) {  
623
          main_in2_ev = 1;  
624
          }  
625
        else {  
626
          }  
627
        if (main_sum_ev == 0) {  
628
          main_sum_ev = 1;  
629
          }  
630
        else {  
631
          }  
632
        if (main_diff_ev == 0) {  
633
          main_diff_ev = 1;  
634
          }  
635
        else {  
636
          }  
637
        if (main_pres_ev == 0) {  
638
          main_pres_ev = 1;  
639
          }  
640
        else {  
641
          }  
642
        if (main_dbl_ev == 0) {  
643
          main_dbl_ev = 1;  
644
          }  
645
        else {  
646
          }  
647
        if (main_zero_ev == 0) {  
648
          main_zero_ev = 1;  
649
          }  
650
        else {  
651
          }  
652
        if (main_clk_ev == 0) {  
653
          main_clk_ev = 1;  
654
          }  
655
        else {  
656
          }  
657
        if (main_clk_pos_edge == 0) {  
658
          main_clk_pos_edge = 1;  
659
          }  
660
        else {  
661
          }  
662
        if (main_clk_neg_edge == 0) {  
663
          main_clk_neg_edge = 1;  
664
          }  
665
        else {  
666
          }  
667
        if (main_clk_pos_edge == 1) {  
668
          N_generate_st = 0;  
669
          }  
670
        else {  
671
          }  
672
        if (main_clk_pos_edge == 1) {  
673
          S1_addsub_st = 0;  
674
          }  
675
        else {  
676
          }  
677
        if (main_clk_pos_edge == 1) {  
678
          S2_presdbl_st = 0;  
679
          }  
680
        else {  
681
          }  
682
        if (main_clk_pos_edge == 1) {  
683
          S3_zero_st = 0;  
684
          }  
685
        else {  
686
          }  
687
        if (main_clk_pos_edge == 1) {  
688
          D_print_st = 0;  
689
          }  
690
        else {  
691
          }  
692
        if (main_in1_ev == 1) {  
693
          main_in1_ev = 2;  
694
          }  
695
        else {  
696
          }  
697
        if (main_in2_ev == 1) {  
698
          main_in2_ev = 2;  
699
          }  
700
        else {  
701
          }  
702
        if (main_sum_ev == 1) {  
703
          main_sum_ev = 2;  
704
          }  
705
        else {  
706
          }  
707
        if (main_diff_ev == 1) {  
708
          main_diff_ev = 2;  
709
          }  
710
        else {  
711
          }  
712
        if (main_pres_ev == 1) {  
713
          main_pres_ev = 2;  
714
          }  
715
        else {  
716
          }  
717
        if (main_dbl_ev == 1) {  
718
          main_dbl_ev = 2;  
719
          }  
720
        else {  
721
          }  
722
        if (main_zero_ev == 1) {  
723
          main_zero_ev = 2;  
724
          }  
725
        else {  
726
          }  
727
        if (main_clk_ev == 1) {  
728
          main_clk_ev = 2;  
729
          }  
730
        else {  
731
          }  
732
        if (main_clk_pos_edge == 1) {  
733
          main_clk_pos_edge = 2;  
734
          }  
735
        else {  
736
          }  
737
        if (main_clk_neg_edge == 1) {  
738
          main_clk_neg_edge = 2;  
739
          }  
740
        else {  
741
          }  
742
        if (N_generate_st == 0) {  
743
          }  
744
        else {  
745
          if (S1_addsub_st == 0) {  
746
            }  
747
          else {  
748
            if (S2_presdbl_st == 0) {  
749
              }  
750
            else {  
751
              if (S3_zero_st == 0) {  
752
                }  
753
              else {  
754
                if (D_print_st == 0) {  
755
                  }  
756
                else {  
757
                  goto while_1_break;  
758
                  }  
759
                }  
760
              }  
761
            }  
762
          }  
763
        }  
764
      }  
765
    while_1_break: ;  
766
    }  
767
  return;  
768
  }  
769
}  
770
  
771
void main () {  
772
//  
773
// Number of lvals: 62  
774
//   Frama_C_interval: int (int min, int max)  
775
//      int (int min, int max)  
776
//   error: void (void)  
777
//      void (void)  
778
//   count: int  
779
//      int  
780
//   res: int  
781
//      int  
782
//   main_in1_val: int  
783
//      int  
784
//   main_in1_val_t: int  
785
//      int  
786
//   main_in1_ev: int  
787
//      int  
788
//   main_in1_req_up: int  
789
//      int  
790
//   main_in2_val: int  
791
//      int  
792
//   main_in2_val_t: int  
793
//      int  
794
//   main_in2_ev: int  
795
//      int  
796
//   main_in2_req_up: int  
797
//      int  
798
//   main_diff_val: int  
799
//      int  
800
//   main_diff_val_t: int  
801
//      int  
802
//   main_diff_ev: int  
803
//      int  
804
//   main_diff_req_up: int  
805
//      int  
806
//   main_sum_val: int  
807
//      int  
808
//   main_sum_val_t: int  
809
//      int  
810
//   main_sum_ev: int  
811
//      int  
812
//   main_sum_req_up: int  
813
//      int  
814
//   main_pres_val: int  
815
//      int  
816
//   main_pres_val_t: int  
817
//      int  
818
//   main_pres_ev: int  
819
//      int  
820
//   main_pres_req_up: int  
821
//      int  
822
//   main_dbl_val: int  
823
//      int  
824
//   main_dbl_val_t: int  
825
//      int  
826
//   main_dbl_ev: int  
827
//      int  
828
//   main_dbl_req_up: int  
829
//      int  
830
//   main_zero_val: int  
831
//      int  
832
//   main_zero_val_t: int  
833
//      int  
834
//   main_zero_ev: int  
835
//      int  
836
//   main_zero_req_up: int  
837
//      int  
838
//   main_clk_val: int  
839
//      int  
840
//   main_clk_val_t: int  
841
//      int  
842
//   main_clk_ev: int  
843
//      int  
844
//   main_clk_req_up: int  
845
//      int  
846
//   main_clk_pos_edge: int  
847
//      int  
848
//   main_clk_neg_edge: int  
849
//      int  
850
//   N_generate_st: int  
851
//      int  
852
//   N_generate_i: int  
853
//      int  
854
//   S1_addsub_st: int  
855
//      int  
856
//   S1_addsub_i: int  
857
//      int  
858
//   S2_presdbl_st: int  
859
//      int  
860
//   S2_presdbl_i: int  
861
//      int  
862
//   S3_zero_st: int  
863
//      int  
864
//   S3_zero_i: int  
865
//      int  
866
//   D_z: int  
867
//      int  
868
//   D_print_st: int  
869
//      int  
870
//   D_print_i: int  
871
//      int  
872
//   N_generate: void (void)  
873
//      void (void)  
874
//   S1_addsub: void (void)  
875
//      void (void)  
876
//   S2_presdbl: void (void)  
877
//      void (void)  
878
//   S3_zero: void (void)  
879
//      void (void)  
880
//   D_print: void (void)  
881
//      void (void)  
882
//   eval: void (void)  
883
//      void (void)  
884
//   start_simulation: void (void)  
885
//      void (void)  
886
//   n1: int  
887
//      int  
888
//   n2: int  
889
//      int  
890
//   n3: int  
891
//      int  
892
//   bound: int  
893
//      int  
894
//   i: int  
895
//      int  
896
//   flag: int  
897
//      int  
898
//  
899
  
900
D_print_i = __VERIFIER_nondet_int();  
901
D_print_st = __VERIFIER_nondet_int();  
902
D_z = __VERIFIER_nondet_int();  
903
N_generate_i = __VERIFIER_nondet_int();  
904
N_generate_st = __VERIFIER_nondet_int();  
905
S1_addsub_i = __VERIFIER_nondet_int();  
906
S1_addsub_st = __VERIFIER_nondet_int();  
907
S2_presdbl_i = __VERIFIER_nondet_int();  
908
S2_presdbl_st = __VERIFIER_nondet_int();  
909
S3_zero_i = __VERIFIER_nondet_int();  
910
S3_zero_st = __VERIFIER_nondet_int();  
911
count = __VERIFIER_nondet_int();  
912
main_clk_ev = __VERIFIER_nondet_int();  
913
main_clk_neg_edge = __VERIFIER_nondet_int();  
914
main_clk_pos_edge = __VERIFIER_nondet_int();  
915
main_clk_req_up = __VERIFIER_nondet_int();  
916
main_clk_val = __VERIFIER_nondet_int();  
917
main_clk_val_t = __VERIFIER_nondet_int();  
918
main_dbl_ev = __VERIFIER_nondet_int();  
919
main_dbl_req_up = __VERIFIER_nondet_int();  
920
main_dbl_val = __VERIFIER_nondet_int();  
921
main_dbl_val_t = __VERIFIER_nondet_int();  
922
main_diff_ev = __VERIFIER_nondet_int();  
923
main_diff_req_up = __VERIFIER_nondet_int();  
924
main_diff_val = __VERIFIER_nondet_int();  
925
main_diff_val_t = __VERIFIER_nondet_int();  
926
main_in1_ev = __VERIFIER_nondet_int();  
927
main_in1_req_up = __VERIFIER_nondet_int();  
928
main_in1_val = __VERIFIER_nondet_int();  
929
main_in1_val_t = __VERIFIER_nondet_int();  
930
main_in2_ev = __VERIFIER_nondet_int();  
931
main_in2_req_up = __VERIFIER_nondet_int();  
932
main_in2_val = __VERIFIER_nondet_int();  
933
main_in2_val_t = __VERIFIER_nondet_int();  
934
main_pres_ev = __VERIFIER_nondet_int();  
935
main_pres_req_up = __VERIFIER_nondet_int();  
936
main_pres_val = __VERIFIER_nondet_int();  
937
main_pres_val_t = __VERIFIER_nondet_int();  
938
main_sum_ev = __VERIFIER_nondet_int();  
939
main_sum_req_up = __VERIFIER_nondet_int();  
940
main_sum_val = __VERIFIER_nondet_int();  
941
main_sum_val_t = __VERIFIER_nondet_int();  
942
main_zero_ev = __VERIFIER_nondet_int();  
943
main_zero_req_up = __VERIFIER_nondet_int();  
944
main_zero_val = __VERIFIER_nondet_int();  
945
main_zero_val_t = __VERIFIER_nondet_int();  
946
res = __VERIFIER_nondet_int();  
947
  
948
  
949
  
950
{  
951
  int n1 = 3;  
952
  int n2 = 5;  
953
  int n3 = 7;  
954
  res = 0;  
955
  auto int bound;  
956
  bound = __VERIFIER_nondet_int();  
957
  __VERIFIER_assume(bound >= 1);  
958
  {  
959
    {  
960
      count = 0;  
961
      main_in1_ev = 2;  
962
      main_in1_req_up = 0;  
963
      main_in2_ev = 2;  
964
      main_in2_req_up = 0;  
965
      main_diff_ev = 2;  
966
      main_diff_req_up = 0;  
967
      main_sum_ev = 2;  
968
      main_sum_req_up = 0;  
969
      main_pres_ev = 2;  
970
      main_pres_req_up = 0;  
971
      main_dbl_ev = 2;  
972
      main_dbl_req_up = 0;  
973
      main_zero_ev = 2;  
974
      main_zero_req_up = 0;  
975
      main_clk_val = 0;  
976
      main_clk_ev = 2;  
977
      main_clk_req_up = 0;  
978
      main_clk_pos_edge = 2;  
979
      main_clk_neg_edge = 2;  
980
      count = 0;  
981
      N_generate_i = 0;  
982
      S1_addsub_i = 0;  
983
      S2_presdbl_i = 0;  
984
      S3_zero_i = 0;  
985
      D_print_i = 0;  
986
            start_simulation();  
987
      }  
988
    {  
989
      int i = 0;  
990
      while (1) {  
991
        if (i < bound) {  
992
          }  
993
        else {  
994
          break;  
995
          }  
996
        {  
997
          if (i % n1 == 0) {  
998
            if (i % n2 == 0) {  
999
              if (i % n3 == 0) {  
1000
                res = i;  
1001
                }  
1002
              else {  
1003
                }  
1004
              }  
1005
            else {  
1006
              }  
1007
            }  
1008
          else {  
1009
            }  
1010
          i ++;  
1011
          int flag = res;  
1012
          while_2_continue: ;  
1013
          {  
1014
            main_clk_val_t = 1;  
1015
            main_clk_req_up = 1;  
1016
                        start_simulation();  
1017
            count ++;  
1018
            }  
1019
  
1020
	  if (res % 105 == 0) {  
1021
	    ;  
1022
	  } else {  
1023
	    error();  
1024
	  }  
1025
	    
1026
          if (count == 5) {  
1027
            if (! (D_z == 0)) {  
1028
              error();  
1029
              }  
1030
            else {  
1031
              }  
1032
            count = 0;  
1033
            }  
1034
          else {  
1035
            }  
1036
          {  
1037
            main_clk_val_t = 0;  
1038
            main_clk_req_up = 1;  
1039
                        start_simulation();  
1040
              
1041
          }  
1042
        }  
1043
      }  
1044
    }  
1045
  }  
1046
return;  
1047
}}  
DateTimeLevelComponentMessage
2023-06-2804:16:58:978INFOCPAMain.detectFrontendLanguageIfNecessaryLanguage C detected and set for analysis
2023-06-2804:16:58:996INFOResourceLimitChecker.fromConfigurationUsing the following resource limits: CPU-time limit of 900s
2023-06-2804:16:59:051INFOCPAchecker.runCPAchecker 2.2 / svcomp23 (OpenJDK 64-Bit Server VM 11.0.19) started
2023-06-2804:16:59:071INFOCPAchecker.parseParsing CFA from file(s) "no_context/combo1.c"
2023-06-2804:17:00:114INFOCoreComponentsFactory.createAlgorithmUsing heuristics to select analysis
2023-06-2804:17:00:125WARNINGCPAchecker.printConfigurationWarningsThe following configuration options were specified but are not used:
cpa.callstack.unsupportedFunctions
termination.violation.witness
cpa.predicate.memoryAllocationsAlwaysSucceed
cpa.arg.compressWitness
cpa.callstack.skipFunctionPointerRecursion
cpa.composite.aggregateBasicBlocks
counterexample.export.graphml
counterexample.export.compressWitness
cpa.arg.proofWitness
2023-06-2804:17:00:126INFOCPAchecker.runAlgorithmStarting analysis ...
2023-06-2804:17:00:130INFOSelectionAlgorithm.chooseConfigPerforming heuristic ...
2023-06-2804:17:00:135INFOAnalysis /home/artjom/CPAchecker-2.2-unix/config/components/svcomp23--multipleLoopsConfig.properties
ResourceLimitChecker.fromConfiguration
Using the following resource limits: CPU-time limit of 900s
2023-06-2804:17:00:149INFOAnalysis /home/artjom/CPAchecker-2.2-unix/config/components/svcomp23--multipleLoopsConfig.properties
CoreComponentsFactory.createAlgorithm
Using Restarting Algorithm
2023-06-2804:17:00:155INFOAnalysis /home/artjom/CPAchecker-2.2-unix/config/components/svcomp23--multipleLoopsConfig.properties
RestartAlgorithm.run
Loading analysis 1 from file /home/artjom/CPAchecker-2.2-unix/config/components/svcomp23--multipleLoops-symbolicExecution.properties ...
2023-06-2804:17:00:160INFOAnalysis /home/artjom/CPAchecker-2.2-unix/config/components/svcomp23--multipleLoopsConfig.properties
NestingAlgorithm.checkConfigs
Mismatch of configuration options when loading from '/home/artjom/CPAchecker-2.2-unix/config/components/svcomp23--multipleLoops-symbolicExecution.properties': 'cpa.composite.aggregateBasicBlocks' has two values 'false' and 'true'. Using 'true'.
2023-06-2804:17:00:161INFOAnalysis /home/artjom/CPAchecker-2.2-unix/config/components/svcomp23--multipleLoopsConfig.properties
NestingAlgorithm.checkConfigs
Mismatch of configuration options when loading from '/home/artjom/CPAchecker-2.2-unix/config/components/svcomp23--multipleLoops-symbolicExecution.properties': 'limits.time.cpu' has two values '900s' and '140s'. Using '140s'.
2023-06-2804:17:00:161INFOAnalysis /home/artjom/CPAchecker-2.2-unix/config/components/svcomp23--multipleLoopsConfig.properties
NestingAlgorithm.checkConfigs
Mismatch of configuration options when loading from '/home/artjom/CPAchecker-2.2-unix/config/components/svcomp23--multipleLoops-symbolicExecution.properties': 'limits.time.cpu::required' has two values '900' and '140s'. Using '140s'.
2023-06-2804:17:00:163INFOAnalysis /home/artjom/CPAchecker-2.2-unix/config/components/svcomp23--multipleLoopsConfig.properties
Analysis /home/artjom/CPAchecker-2.2-unix/config/components/svcomp23--multipleLoops-symbolicExecution.properties
ResourceLimitChecker.fromConfiguration
Using the following resource limits: CPU-time limit of 140s
2023-06-2804:17:00:464INFOAnalysis /home/artjom/CPAchecker-2.2-unix/config/components/svcomp23--multipleLoopsConfig.properties
RestartAlgorithm.run
Starting analysis 1 ...
2023-06-2804:19:07:182WARNINGAnalysis /home/artjom/CPAchecker-2.2-unix/config/components/svcomp23--multipleLoopsConfig.properties
ShutdownNotifier.shutdownIfNecessary
Warning: Analysis 1 stopped. (The CPU-time limit of 140s has elapsed.)
2023-06-2804:19:07:372INFOAnalysis /home/artjom/CPAchecker-2.2-unix/config/components/svcomp23--multipleLoopsConfig.properties
RestartAlgorithm.run
RestartAlgorithm switches to the next configuration...
2023-06-2804:19:07:372INFOAnalysis /home/artjom/CPAchecker-2.2-unix/config/components/svcomp23--multipleLoopsConfig.properties
RestartAlgorithm.run
Loading analysis 2 from file /home/artjom/CPAchecker-2.2-unix/config/components/svcomp23--multipleLoops-valueAnalysis-Cegar.properties ...
2023-06-2804:19:07:375INFOAnalysis /home/artjom/CPAchecker-2.2-unix/config/components/svcomp23--multipleLoopsConfig.properties
NestingAlgorithm.checkConfigs
Mismatch of configuration options when loading from '/home/artjom/CPAchecker-2.2-unix/config/components/svcomp23--multipleLoops-valueAnalysis-Cegar.properties': 'cpa.composite.aggregateBasicBlocks' has two values 'false' and 'true'. Using 'true'.
2023-06-2804:19:07:375INFOAnalysis /home/artjom/CPAchecker-2.2-unix/config/components/svcomp23--multipleLoopsConfig.properties
NestingAlgorithm.checkConfigs
Mismatch of configuration options when loading from '/home/artjom/CPAchecker-2.2-unix/config/components/svcomp23--multipleLoops-valueAnalysis-Cegar.properties': 'limits.time.cpu' has two values '900s' and '60s'. Using '60s'.
2023-06-2804:19:07:376INFOAnalysis /home/artjom/CPAchecker-2.2-unix/config/components/svcomp23--multipleLoopsConfig.properties
NestingAlgorithm.checkConfigs
Mismatch of configuration options when loading from '/home/artjom/CPAchecker-2.2-unix/config/components/svcomp23--multipleLoops-valueAnalysis-Cegar.properties': 'limits.time.cpu::required' has two values '900' and '60s'. Using '60s'.
2023-06-2804:19:07:376INFOAnalysis /home/artjom/CPAchecker-2.2-unix/config/components/svcomp23--multipleLoopsConfig.properties
Analysis /home/artjom/CPAchecker-2.2-unix/config/components/svcomp23--multipleLoops-valueAnalysis-Cegar.properties
ResourceLimitChecker.fromConfiguration
Using the following resource limits: CPU-time limit of 60s
2023-06-2804:19:07:429INFOAnalysis /home/artjom/CPAchecker-2.2-unix/config/components/svcomp23--multipleLoopsConfig.properties
RestartAlgorithm.run
Starting analysis 2 ...
2023-06-2804:19:07:522INFOCPAchecker.runAlgorithmStopping analysis ...
Statistics NameStatistics ValueAdditional Value
Selection Algorithm statistics
Size of preliminary analysis reached set 0
Used algorithm property /home/artjom/CPAchecker-2.2-unix/config/components/svcomp23--multipleLoopsConfig.properties
Program containing only relevant bools 0
Relevant boolean vars / relevant vars ratio 0.0685
Requires alias handling 0
Requires loop handling 1
Has a single loop 0
Requires composite-type handling 0
Requires array handling 0
Requires float handling 0
Requires recursion handling 0
Relevant addressed vars / relevant vars ratio 0.0000
Program containing external functions true
Number of all righthand side functions 9
Restart Algorithm statistics
Number of algorithms provided 7
Number of algorithms used 2
Total time for algorithm 2 0.150s
ValueAnalysisCPA statistics
Number of variables per state 0.00 sum: 0, count: 1449, min: 0, max: 0
Number of global variables per state 0.00 sum: 0, count: 1449, min: 0, max: 0
Number of assumptions 670
Number of deterministic assumptions 0
Level of Determinism 0%
ValueAnalysisPrecisionAdjustment statistics
Number of abstraction computations 1782
Total time for liveness abstraction 0.000s
Total time for abstraction computation 0.004s
Total time for path thresholds 0.000s
ConstraintsStrengthenOperator statistics
Total time for strengthening by ConstraintsCPA 0.000s
Replaced symbolic expressions 0
AutomatonAnalysis (SVCOMP) statistics
Number of states 1
Total time for successor computation 0.000s
Automaton transfers with branching 0
Automaton transfer successors 1.00 sum: 2120, count: 2120, min: 1, max: 1 [1 x 2120]
Number of states with assumption transitions 0
CPA algorithm statistics
Number of iterations 1449
Max size of waitlist 22
Average size of waitlist 12
Number of computed successors 1782
Max successors for one state 2
Number of times merged 0
Number of times stopped 334
Number of times breaked 0
Total time for CPA algorithm 0.082s Max: 0.082s
Time for choose from waitlist 0.017s
Time for precision adjustment 0.011s
Time for transfer relation 0.024s
Time for stop operator 0.003s
Time for adding to reached set 0.023s
ValueAnalysisRefiner statistics
Number of refinements 0
Number of targets found 0 count: 0, min: 0, max: 0, avg: 0.00
Time for completing refinement 0.000s
Number of root relocations 0
Number of similar, repeated refinements 0
Number of unique precision increments 0
PathExtractor statistics
Total number of targets found 0
ValueAnalysisPathInterpolator statistics
Time for interpolation 0.000s
Number of interpolations 0
Number of interpolation queries 0 count: 0, min: 0, max: 0, avg: 0.00
Size of interpolant 0.00 sum: 0, count: 0, min: 0, max: 0
Number of sliced prefixes 0 count: 0, min: 0, max: 0, avg: 0.00
Extracting infeasible sliced prefixes 0.000s
Selecting infeasible sliced prefixes 0.000s
CEGAR algorithm statistics
Number of CEGAR refinements 0
Counterexample-Check Algorithm statistics
Number of counterexample checks 0
CPA algorithm statistics
Number of iterations 1449
Max size of waitlist 22
Average size of waitlist 12
Number of computed successors 1782
Max successors for one state 2
Number of times merged 0
Number of times stopped 334
Number of times breaked 0
Total time for CPA algorithm 0.082s Max: 0.082s
Time for choose from waitlist 0.017s
Time for precision adjustment 0.011s
Time for transfer relation 0.024s
Time for stop operator 0.003s
Time for adding to reached set 0.023s
ValueAnalysisRefiner statistics
Number of refinements 0
Number of targets found 0 count: 0, min: 0, max: 0, avg: 0.00
Time for completing refinement 0.000s
Number of root relocations 0
Number of similar, repeated refinements 0
Number of unique precision increments 0
PathExtractor statistics
Total number of targets found 0
ValueAnalysisPathInterpolator statistics
Time for interpolation 0.000s
Number of interpolations 0
Number of interpolation queries 0 count: 0, min: 0, max: 0, avg: 0.00
Size of interpolant 0.00 sum: 0, count: 0, min: 0, max: 0
Number of sliced prefixes 0 count: 0, min: 0, max: 0, avg: 0.00
Extracting infeasible sliced prefixes 0.000s
Selecting infeasible sliced prefixes 0.000s
CEGAR algorithm statistics
Number of CEGAR refinements 0
Counterexample-Check Algorithm statistics
Number of counterexample checks 0
Code Coverage
Function coverage 1.000
Visited lines 455
Total lines 455
Line coverage 1.000
Visited conditions 234
Total conditions 234
Condition coverage 1.000
CPAchecker general statistics
Number of program locations 732
Number of CFA edges (per node) 861 count: 732, min: 0, max: 3, avg: 1.18
Number of relevant variables 73
Number of functions 9
Number of loops (and loop nodes) 3 sum: 294, min: 40, max: 196, avg: 98.00
Size of reached set 1449
Number of reached locations 514 70%
Avg states per location 2
Max states per location 3 at node N7
Number of reached functions 9 100%
Number of target states 0
Time for analysis setup 1.055s
Time for loading CPAs 0.179s
Time for loading parser 0.156s
Time for CFA construction 0.693s
Time for parsing file(s) 0.262s
Time for AST to CFA 0.167s
Time for CFA sanity check 0.048s
Time for post-processing 0.152s
Time for CFA export 0.846s
Time for function pointers resolving 0.005s
Function calls via function pointers 0 count: 1, min: 0, max: 0, avg: 0.00
Instrumented function pointer calls 0 count: 1, min: 0, max: 0, avg: 0.00
Function calls with function pointer arguments 0 count: 1, min: 0, max: 0, avg: 0.00
Instrumented function pointer arguments 0 count: 1, min: 0, max: 0, avg: 0.00
Time for classifying variables 0.090s
Time for collecting variables 0.033s
Time for solving dependencies 0.001s
Time for building hierarchy 0.000s
Time for building classification 0.051s
Time for exporting data 0.005s
Time for Analysis 127.396s
CPU time for analysis 141.440s
Time for analyzing result 0.001s
Total time for CPAchecker 128.452s
Total CPU time for CPAchecker 144.560s
Time for statistics 0.051s
Time for Garbage Collector 0.936s in 55 runs
Garbage Collector(s) used G1 Old Generation, G1 Young Generation
Used heap memory 475MB ( 453 MiB) max; 230MB ( 219 MiB) avg; 481MB ( 459 MiB) peak
Used non-heap memory 53MB ( 50 MiB) max; 50MB ( 48 MiB) avg; 53MB ( 51 MiB) peak
Used in G1 Old Gen pool 94MB ( 90 MiB) max; 61MB ( 58 MiB) avg; 94MB ( 90 MiB) peak
Allocated heap memory 638MB ( 609 MiB) max; 544MB ( 519 MiB) avg
Allocated non-heap memory 56MB ( 53 MiB) max; 53MB ( 51 MiB) avg
Total process virtual memory 12292MB ( 11723 MiB) max; 12284MB ( 11715 MiB) avg
#Configuration NameConfiguration Value
1analysis.entryFunction main
2analysis.name svcomp23
3analysis.programNames no_context/combo1.c
4analysis.selectAnalysisHeuristically true
5analysis.summaryEdges true
6cfa.simplifyCfa false
7cfa.useCFACloningForMultiThreadedPrograms true
8counterexample.export.compressWitness false
9counterexample.export.graphml witness.graphml
10cpa.arg.compressWitness false
11cpa.arg.proofWitness witness.graphml
12cpa.callstack.skipFunctionPointerRecursion true
13cpa.callstack.unsupportedFunctions pthread_create,pthread_key_create,sin,cos,__builtin_uaddl_overflow
14cpa.composite.aggregateBasicBlocks false
15cpa.predicate.memoryAllocationsAlwaysSucceed true
16datarace.config svcomp23--datarace.properties
17heuristicSelection.addressedRatio 0.0
18heuristicSelection.complexLoopConfig components/svcomp23--configselection-restart-valueAnalysis-fallbacks.properties
19heuristicSelection.loopConfig components/svcomp23--multipleLoopsConfig.properties
20heuristicSelection.loopFreeConfig components/svcomp23--configselection-restart-bmc-fallbacks.properties
21heuristicSelection.singleLoopConfig components/svcomp23--singleLoopConfig.properties
22language C
23limits.time.cpu 900s
24limits.time.cpu::required 900
25log.level INFO
26memorycleanup.config svcomp23--memorycleanup.properties
27memorysafety.config svcomp23--memorysafety.properties
28overflow.config svcomp23--overflow.properties
29parser.usePreprocessor true
30specification /home/artjom/CPAchecker-2.2-unix/config/properties/unreach-call.prp
31statistics.print true
32termination.config svcomp23--termination.properties
33termination.violation.witness witness.graphml

About

This table was generated by CPAchecker. For feedback, questions, and bug reports please use our issue tracker.

License: Apache 2.0 License

This application includes third-party dependencies under different licenses. Click here to view them.

{{dependency.name}} {{dependency.version}}

Source: {{dependency.repository}}

{{dependency.copyright}}

License:

Full text of license
{{dependencies.licenses[dependency.licenseId]}}